Nuprl Lemma : adjacent-to-same 11,40

T:Type, L:(T List), abc:T.
no_repeats(T;L adjacent(T;L;a;b adjacent(T;L;a;c (b = c
latex


Definitionss = t, x:AB(x), x:AB(x), Type, type List, no_repeats(T;l), adjacent(T;L;x;y), left + right, P  Q, x before y  l, P  Q, t  T, False, A
Lemmasl before antisymmetry, adjacent-before, adjacent wf, no repeats wf, before-adjacent2, l before wf

origin